(set-info :source |fuzzsmt|)
(set-info :smt-lib-version 2.0)
(set-info :category "random")
(set-info :status unknown)
(set-logic QF_BV)
(declare-fun v0 () (_ BitVec 26))
(declare-fun v1 () (_ BitVec 5))
(declare-fun v2 () (_ BitVec 9))
(declare-fun v3 () (_ BitVec 23))
(declare-fun v4 () (_ BitVec 8))
(assert (let ((e5(_ bv8 7)))
(let ((e6 (bvsub ((_ sign_extend 21) v1) v0)))
(let ((e7 (bvsrem ((_ zero_extend 2) e5) v2)))
(let ((e8 ((_ repeat 3) e7)))
(let ((e9 (ite (= (_ bv1 1) ((_ extract 3 3) v4)) ((_ zero_extend 21) v1) e6)))
(let ((e10 (bvadd e6 e9)))
(let ((e11 (bvor v3 ((_ sign_extend 16) e5))))
(let ((e12 (bvuge e11 ((_ zero_extend 15) v4))))
(let ((e13 (bvuge ((_ zero_extend 14) v2) v3)))
(let ((e14 (bvule e11 ((_ sign_extend 14) e7))))
(let ((e15 (= ((_ zero_extend 1) v4) v2)))
(let ((e16 (bvsge ((_ sign_extend 3) v3) e10)))
(let ((e17 (= e6 v0)))
(let ((e18 (distinct ((_ sign_extend 19) v4) e8)))
(let ((e19 (bvule v3 e11)))
(let ((e20 (bvugt e8 ((_ zero_extend 1) v0))))
(let ((e21 (bvugt e6 ((_ zero_extend 19) e5))))
(let ((e22 (bvuge v0 ((_ sign_extend 17) e7))))
(let ((e23 (bvugt ((_ sign_extend 1) v4) v2)))
(let ((e24 (bvult ((_ zero_extend 3) v3) e9)))
(let ((e25 (= ((_ zero_extend 3) v1) v4)))
(let ((e26 (and e20 e17)))
(let ((e27 (or e22 e12)))
(let ((e28 (ite e24 e24 e24)))
(let ((e29 (=> e13 e19)))
(let ((e30 (ite e29 e23 e23)))
(let ((e31 (or e25 e18)))
(let ((e32 (and e30 e31)))
(let ((e33 (and e28 e21)))
(let ((e34 (ite e33 e32 e27)))
(let ((e35 (=> e26 e16)))
(let ((e36 (xor e15 e15)))
(let ((e37 (= e35 e14)))
(let ((e38 (not e36)))
(let ((e39 (or e38 e34)))
(let ((e40 (= e37 e39)))
(let ((e41 (and e40 (not (= v2 (_ bv0 9))))))
(let ((e42 (and e41 (not (= v2 (bvnot (_ bv0 9)))))))
e42
)))))))))))))))))))))))))))))))))))))))

(check-sat)
